D:Dsys, i:Id, s:M(i).(timed)state. stutter-state(s)  d-world-state(D;i) 

latex

Definitions	t  T, x:A. B(x), mlnk(m), source(l), Id, s = t, M(i), M.Msg, {x:A| B(x)} , type List, [], d-decl(D;i), null, <a, b>, shift-state(s), stutter-state(s), d-world-state(D;i), Dsys, M.(timed)state
Lemmas	ma-tst wf, dsys wf, shift-state wf, null-action wf, d-decl wf, ma-msg wf, d-m wf, Id wf, lsrc wf, mlnk wf d